Inductive Instr : Type :=
  | instr_skip          : Instr
  | instr_assign_bool   : Id      -> BoolExp   -> Instr
  | instr_assign_nat    : Id      -> ArithExp  -> Instr
  | instr_assign_int    : Id      -> ArithExp  -> Instr
  | instr_assign_byte   : Id      -> ByteExp   -> Instr
  | instr_assign_matrix : Id      -> MatrixExp -> Instr
  | instr_seq           : Instr   -> Instr     -> Instr
  | instr_if            : BoolExp -> Instr     -> Instr -> Instr
  | instr_while         : BoolExp -> Instr     -> Instr
  | instr_for           : Id      -> ArithExp  -> Instr -> Instr
  | instr_matrix_set    : Id      -> ArithExp  -> ArithExp -> ByteExp -> Instr
.